Incorporating Decision Procedures in Implicit Induction
Identifieur interne : 008F50 ( Main/Exploration ); précédent : 008F49; suivant : 008F51Incorporating Decision Procedures in Implicit Induction
Auteurs : Alessandro Armando ; Michael Rusinowitch ; Sorin StratulatSource :
English descriptors
Abstract
As many proof obligations in system verification require complex interleaving of pure logic and domain-specific steps, a crucial activity in the construction of a successful verification tool is the effective incorporation of reasoning specialists (such as decision procedures or unification algorithms) within more general inference modules (such as rewrite engines or inference procedures for reasoning by induction). Mathematical induction is a fundamental reasoning technique for system verification. In the last decades it has been thoroughly investigated and several powerful techniques and heuristics for reasoning about inductively defined objects have been put forward \cite{bm79,KNZ91 :jsc,JAR : :BouhoulaR1995}. These techniques allow the automatic discharge of many non trivial proof-obligations. Yet---when applied to verification problems of practical significance---the level of automation provided by such techniques is still unsatisfactory. The seminal work by Boyer \& Moore \cite{bm88} showed that a higher level of automation can be achieved by induction provers thanks to the incorporation of decision procedures. However in Boyer \& Moore's approach the interplay of the decision procedure is limited to the simplification engine and therefore it does not exploit the potentials of the cooperation between the decision procedure and the induction heuristics which are best illustrated by means of the following example. Let us consider the following proof-obligation occurring in the verification proof of the MJRTY algorithm \cite{bm91} given in \cite{str98b,str00b} : \begin{align} \label{eq :6} a\neq mc(p,i)\Rightarrow 2*(ml(p,i)+count(p,i,a))< ml(p,i'), \textit{Noname} = access(p,i') \Rightarrow \\ 2*((ml(p,i')-1)+s(count(p,i',\textit{Noname})))<> et nous validons les modèles à l'aide de l'AtelierB
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Crin, to step Corpus: 002D67
- to stream Crin, to step Curation: 002D67
- to stream Crin, to step Checkpoint: 001566
- to stream Main, to step Merge: 009471
- to stream Main, to step Curation: 008F50
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="409">Incorporating Decision Procedures in Implicit Induction</title></titleStmt><publicationStmt><idno type="RBID">CRIN:armando01a</idno><date when="2001" year="2001">2001</date><idno type="wicri:Area/Crin/Corpus">002D67</idno><idno type="wicri:Area/Crin/Curation">002D67</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">002D67</idno><idno type="wicri:Area/Crin/Checkpoint">001566</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Checkpoint">001566</idno><idno type="wicri:Area/Main/Merge">009471</idno><idno type="wicri:Area/Main/Curation">008F50</idno><idno type="wicri:Area/Main/Exploration">008F50</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Incorporating Decision Procedures in Implicit Induction</title><author><name sortKey="Armando, Alessandro" sort="Armando, Alessandro" uniqKey="Armando A" first="Alessandro" last="Armando">Alessandro Armando</name></author><author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michael" last="Rusinowitch">Michael Rusinowitch</name></author><author><name sortKey="Stratulat, Sorin" sort="Stratulat, Sorin" uniqKey="Stratulat S" first="Sorin" last="Stratulat">Sorin Stratulat</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>integration of reasoning modules</term><term>proof by implicit induction</term><term>rewriting</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en" wicri:score="7058">As many proof obligations in system verification require complex interleaving of pure logic and domain-specific steps, a crucial activity in the construction of a successful verification tool is the effective incorporation of reasoning specialists (such as decision procedures or unification algorithms) within more general inference modules (such as rewrite engines or inference procedures for reasoning by induction). Mathematical induction is a fundamental reasoning technique for system verification. In the last decades it has been thoroughly investigated and several powerful techniques and heuristics for reasoning about inductively defined objects have been put forward \cite{bm79,KNZ91 :jsc,JAR : :BouhoulaR1995}. These techniques allow the automatic discharge of many non trivial proof-obligations. Yet---when applied to verification problems of practical significance---the level of automation provided by such techniques is still unsatisfactory. The seminal work by Boyer \& Moore \cite{bm88} showed that a higher level of automation can be achieved by induction provers thanks to the incorporation of decision procedures. However in Boyer \& Moore's approach the interplay of the decision procedure is limited to the simplification engine and therefore it does not exploit the potentials of the cooperation between the decision procedure and the induction heuristics which are best illustrated by means of the following example. Let us consider the following proof-obligation occurring in the verification proof of the MJRTY algorithm \cite{bm91} given in \cite{str98b,str00b} : \begin{align} \label{eq :6} a\neq mc(p,i)\Rightarrow 2*(ml(p,i)+count(p,i,a))< ml(p,i'), \textit{Noname} = access(p,i') \Rightarrow \\ 2*((ml(p,i')-1)+s(count(p,i',\textit{Noname})))<> et nous validons les modèles à l'aide de l'AtelierB</div></front></TEI><affiliations><list></list><tree><noCountry><name sortKey="Armando, Alessandro" sort="Armando, Alessandro" uniqKey="Armando A" first="Alessandro" last="Armando">Alessandro Armando</name><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michael" last="Rusinowitch">Michael Rusinowitch</name><name sortKey="Stratulat, Sorin" sort="Stratulat, Sorin" uniqKey="Stratulat S" first="Sorin" last="Stratulat">Sorin Stratulat</name></noCountry></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 008F50 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 008F50 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= CRIN:armando01a
|texte= Incorporating Decision Procedures in Implicit Induction
}}
| This area was generated with Dilib version V0.6.33. |  |